1. Field
The present invention relates generally to functional verification of circuit designs and, more particularly, to the generation of verification vectors for use in debugging circuit designs.
2. Description of the Related Art
Verification is typically the most time-consuming component in a circuit design process. Failing to detect functional design errors early in the design stage usually leads to the expensive re-spin of the design process. This re-spin includes diagnosis and correction of the errors, logic and physical re-synthesis, and most important of all, re-running the functional verification of the design.
Thus far, simulation is the mainstream approach for function verification of circuit designs. Various coverage metrics, for example, hardware description language (HDL)-based code coverage, are used to assess the quality of the verification vectors and determine when to stop the simulation process. A drawback is that the verification vectors are either manually derived by designers or randomly generated from the high-level description of the design and its environment. As a result, verification vectors, for example, for some corner-case bugs, are not easily derived and high coverage is generally hard to achieve.
Deterministic functional vector generation is one technique intended to enhance the aforementioned verification quality. Deterministic functional vector generation can be viewed as a constraint satisfiability problem. Intended circuit behavior is translated as a set of temporal constraints and a design error is found or detected if there exists an input sequence that violates these constraints. However, due to the increasing complexity of modern circuit designs, current constraint satisfiability techniques still suffer from unacceptable capacity and performance problems. For example, typical Automatic Test Pattern Generation (ATPG) and Boolean satisfiability (SAT) engines use branch-and-bound algorithms to search for test vectors in the Boolean space. These techniques can be used to generate counter-examples for the properties of a circuit. However, because the computational complexity of these techniques grows exponentially as the sequentiality of the property increases, these techniques can only handle property checking with limited sequential depth.
In contrast, general arithmetic solvers apply mathematical theorems to analyze the constraints. They treat the signals in a circuit as integers and solve the formulas in the integral or floating point number system. However, since the signal values of the circuit actually operate in the modular number system, solving circuit constraints in the integral or floating point number system may add unnecessary complexity and even lead to invalid solutions.
Finite State Machine (FSM) reachability analysis is another technique intended to enhance the aforementioned verification quality. FSM state traversal techniques treat the design as a finite state machine and the properties as temporal relations between states. In order to assure that no input sequence can violate the properties, a complete state reachability analysis is required. Explicit state enumeration approach is a technique for performing the analysis that uses a hash data structure to record the reached states. Since the number of states grows exponentially as the number of registers increases, the explicit state enumeration technique has the state explosion problem for larger designs.
Symbolic state traversal approach is another technique for performing the reachability analysis. In contrast to the explicit approach, symbolic state traversal approach uses compact data structures such as Binary Decision Diagram (BDD) to compute and record the reached states. In general, symbolic state traversal approach can handle larger designs than the explicit state enumeration approach. However, symbolic state traversal approach still suffers from the state explosion problem for designs with more than approximately one hundred registers. As a result, full chip (whole circuit) functional verification is unattainable using FSM state traversal techniques.